\begin{figure*}[t]
	\center
	\resizebox{\textwidth}{!}{\includegraphics{results.pdf}}
	\caption{\textbf{Performance Results:} The four figures above show the performance results measured using the \textsc{ASMS} application (figures on the left) and using the \textsc{MS} application (figures on the right), with the increase in the application state size (top figures) and the increase in the size of the rule state (bottom figures).}	
	\label{fig:results}
\end{figure*}


\subsection{Translational Semantics}
\label{sec:TranslationalSemantics}

\SAR's semantics is captured by translating models into Prolog. This has several advantages: this translation gives \SAR a formal semantics in terms of First-Order Logic, as the underlying theory behind Prolog; second, matching expressions from the \texttt{DynamicBinding} part is easily resolved with Prolog because the patterns are simply translated into queries.

A \SAR model is translated as follows: the \texttt{StaticMapping} and the \texttt{Dynamic\-Sta\-te} parts are translated as facts, the \texttt{SecurityRules} and the \texttt{DynamicBinding} expressions are straightforwardly translated into rules. When an access to methods involved in policy actions is requested, the Policy Management Logic (\textsc{Pl}) computes if the current dynamic configuration and the security policy allow this method call, using the following Prolog rules:

\medskip\noindent
\begin{minipage}{\textwidth}
\begin{small}
			\begin{sffamily}
\begin{tabular}{l c l}
allow\_operation(S,A,T) &$\leftarrow$\;& operation(S,A,T),\\
&& permitted(\_,S,A,T),\\
 &&$\lnot$ prohibited(\_,S,A,T).\\
permitted(I,S,A,T)    &$\leftarrow$\;& permission(I,$R_s$,A,$R_t$,C),\\ 
&&instance\_of(S,$R_s$), action(A),\\
                                    && instance\_of(T,$R_t$), hold(S,A,T,C).\\
prohibited(I,S,A,T)     &$\leftarrow$\;& prohibition(I,$R_s$,A,$R_t$,C),\\
&& instance\_of(S,$R_s$), action(A),\\
                                    && instance\_of(T,$R_t$), hold(S,A,T,C).
\end{tabular}
			\end{sffamily}
\end{small}
\end{minipage}
\medskip

\noindent These rules state that an access is granted if it is permitted but not prohibited. This is a management choice: an implicit priority is given to prohibitions over permissions for resolving potential conflicts. Obligations are managed as follows \cite{Elrakaiby2011}\footnote{We simplify the presentation of obligation management for convenience.}: if the activation context of an obligation, for a subject \textsf{s} to take some action \textsf{a} on a target \textsf{t}, holds at a state at time \textsf{timestamp}, then a fact \textsf{obl(s,a,t,activated,timestamp)} is inserted into the policy state. At the same time, the violation context of the obligation is checked: if it contains a \textsf{delay} context, an external timer is triggered. This timer notifies the policy engine at the elapse of the specified delay to reevaluate the obligation. An activated obligation is fulfilled if it is satisfied before its violation context holds, otherwise it is violated. Interested readers are referred to \cite{Elrakaiby2011,Cuppens2003} for a complete presentation of the underlying formal access control and obligation models, and their formal operational semantics. Conflicts between obligations and prohibitions are resolved similarly by prioritizing obligations. 

The framework presented in this paper can be extended with advanced features (e.g., delegation \cite{Ben-Ghorbel-Talbi2010}, or more advanced conflict detection mechanisms and resolution strategies \cite{Cuppens2007c}) by using the MotOr\textsc{Bac} policy management engine \cite{autrel2008motorbac}. 






%\noindent The previous rules state that an operation is allowed if it is authorized but not prohibited by the policy. This means that in our framework an implicit priority is given to prohibitions over permissions to resolve potential conflicts between permissions and prohibitions\footnote{Interested readers are referred to \cite{Elrakaiby2011,Cuppens2003} for more complete presentation of the formal access control logic model.}. This work can be extended to support more advanced features such as delegation \cite{Ben-Ghorbel-Talbi2010} and more advanced conflict detection and resolution strategies \cite{Cuppens2007c}. 

%The management of obligation rules follows the obligation model presented in \cite{Elrakaiby2011} where the formal operational semantics is given. In the following, we only sketch obligation management: obligations are managed according to the obligation state model in Figure \ref{fig_obligation}. The figure shows the different states of an obligation: The obligation is initially abstract, when the obligation activation context becomes true for a particular subject $S$, the obligation is instantiated for this subject and its state becomes active. An activated obligation is called a {\it concrete} obligation. The obligation state is then managed similarly according to changes detected in the obligation contexts. Note that we do not show the deactivation/cancellation of obligations to simplify the figure. 

%\begin{figure}[t]
	%\center
%%	\resizebox{\textwidth}{!}
	%\includegraphics[width=5cm]{obligation.pdf}
	%\caption{Obligation Management}
	%\label{fig_obligation}
%\end{figure}

